ds:(IdType), da:(IdKndType), A1, B1, A2, B2:Type.
(A2 r A1)  (B1 r B2)  (Component(ds;da;A1;B1) r Component(ds;da;A2;B2)) 

latex

Definitions	x. t(x), RealizerScheme{i:l}(), x,y. t(x;y), a:A fp B(a), t  T, Interface(ds;da;A), Component(ds;da;A;B), P  Q, x:A. B(x), x(s), x(s1,s2),
Lemmas	subtype rel product, es realizer wf, Namer wf, nat wf, interface-subtype, interface wf, RealizerScheme wf, Id wf, hasloc wf, assert wf, Knd wf, top wf, locknd-spread wf2, l member wf, LocKnd wf, subtype rel function